home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 4 / Apprentice-Release4.iso / Languages / Caml Light 0.7 / examples / kb / order.ml < prev    next >
Encoding:
Text File  |  1995-06-19  |  2.6 KB  |  80 lines  |  [TEXT/MPS ]
  1. (*********************** Recursive Path Ordering ****************************)
  2.  
  3. #open "terms";;
  4.  
  5. type ordering = Greater | Equal | NotGE;;
  6.  
  7. let ge_ord order pair = match order pair with NotGE -> false | _ -> true
  8. and gt_ord order pair = match order pair with Greater -> true | _ -> false
  9. and eq_ord order pair = match order pair with Equal -> true | _ -> false
  10. ;;
  11.  
  12. let rem_eq equiv = remrec where rec remrec x = function
  13.      []  -> failwith "rem_eq"
  14.   | y::l -> if equiv (x,y) then l else y :: remrec x l
  15. ;;
  16.  
  17. let diff_eq equiv (x,y) =
  18.   let rec diffrec = function
  19.       ([],_) as p -> p
  20.     | (h::t, y)   -> try diffrec (t,rem_eq equiv h y)
  21.                      with Failure _ ->
  22.                        let (x',y') = diffrec (t,y) in (h::x',y') in
  23.   if list_length x > list_length y then
  24.     let (y',x') = diffrec(y,x) in (x', y')
  25.   else
  26.     diffrec(x,y)
  27. ;;
  28.  
  29. (* multiset extension of order *)
  30. let mult_ext order = function
  31.     Term(_,sons1), Term(_,sons2) ->
  32.       begin match diff_eq (eq_ord order) (sons1,sons2) with
  33.            ([],[]) -> Equal
  34.          | (l1,l2) ->
  35.               if for_all (fun n -> exists (fun m -> order(m,n)=Greater) l1) l2
  36.               then Greater else NotGE
  37.       end
  38.   | _ -> failwith "mult_ext"
  39. ;;
  40.  
  41. (* lexicographic extension of order *)
  42. let lex_ext order = function
  43.     (Term(_,sons1) as m), (Term(_,sons2) as n) ->
  44.       let rec lexrec = function
  45.         ([] , []) -> Equal
  46.       | ([] , _ ) -> NotGE
  47.       | ( _ , []) -> Greater
  48.       | (x1::l1, x2::l2) ->
  49.           match order (x1,x2) with
  50.             Greater -> if for_all (fun n' -> gt_ord order (m,n')) l2 
  51.                        then Greater else NotGE
  52.           | Equal -> lexrec (l1,l2)
  53.           | NotGE -> if exists (fun m' -> ge_ord order (m',n)) l1 
  54.                      then Greater else NotGE in
  55.       lexrec (sons1, sons2)
  56.   | _ -> failwith "lex_ext"
  57. ;;
  58.  
  59. (* recursive path ordering *)
  60. let rpo op_order ext = rporec
  61.   where rec rporec (m,n) =
  62.     if m=n then Equal else 
  63.       match m with
  64.           Var m -> NotGE
  65.         | Term(op1,sons1) ->
  66.             match n with
  67.                 Var n ->
  68.                   if occurs n m then Greater else NotGE
  69.               | Term(op2,sons2) ->
  70.                   match (op_order op1 op2) with
  71.                       Greater ->
  72.                         if for_all (fun n' -> gt_ord rporec (m,n')) sons2
  73.                         then Greater else NotGE
  74.                     | Equal ->
  75.                         ext rporec (m,n)
  76.                     | NotGE ->
  77.                         if exists (fun m' -> ge_ord rporec (m',n)) sons1
  78.                         then Greater else NotGE
  79. ;;
  80.